Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 56b78a0ed104c896c033bcd2284449cea2dd5d12 --onto 0196bca784f82f90b4efd2a85a400daf4ab767f8. (2024-09-27 21:52:40)

!bench to ensure the code doesn't introduce non trivial regressions.

I'm also not exactly sure that this is the proper solution for the instantiateMVars time leak. This is only going to profile it in very specific situations, a more uniform solution seems more desirable to me? But also potentially more threatening to performance.

Here are the benchmark results for commit e78addd.
There were significant changes against commit 56b78a0:

  Benchmark                 Metric       Change
  =======================================================
+ import Lean               task-clock   -11.4% (-12.9 σ)
+ import Lean               wall-clock   -11.5% (-12.9 σ)
+ lake config tree          task-clock    -9.3% (-17.4 σ)
+ lake config tree          wall-clock    -9.3% (-16.7 σ)
+ language server startup   task-clock    -1.8% (-13.6 σ)
+ language server startup   wall-clock    -1.8% (-10.4 σ)

I'm also not exactly sure that this is the proper solution for the instantiateMVars time leak. This is only going to profile it in very specific situations, a more uniform solution seems more desirable to me? But also potentially more threatening to performance.

Fair point. It should be noted that instantiateMVarsProfiling was already a thing, I just expanded its use and ensured it has a trace node so that it shows up in the trace profiler also, previously it would only show up in the other profiler.

The proper solution would be to add a trace node to instantiateMVars itself, I agree, but that is a lot trickier. Lean.Util.Trace (which defines the trace machinery) imports Lean.MetavarContext (where instantiateMVars lives), so we'd have to figure out why this is, and I suspect we'd have to split MetavarContext up.

@hargoniX, since you added thumbs-up to my last comment, does that mean you approve of the change in this PR, or do you think we should do the "proper" solution and rip up instantiateMVars to add a trace node directly?

I do understand why you did what you did now. But I do not have enough knowledge about our meta internals to know what exactly would be required here. Someone else from the team would have to weigh in.

awaiting-review

Probably helps if I put that tag on. I'll be away for the next two/three weeks, though, so I won't respond to any review comments until then